/*
 * Alloy Analyzer 4 -- Copyright (c) 2006-2008, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

package edu.ut.ece382c.valloy.ast;

import java.util.List;
import java.util.Vector;

import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorFatal;
import edu.mit.csail.sdg.alloy4.ErrorType;
import edu.mit.csail.sdg.alloy4.ErrorSyntax;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.SafeList;
import edu.mit.csail.sdg.alloy4.Util;
import edu.ut.ece382c.valloy.parser.Decl;

/** Mutable; represents a signature. */

public class Sig extends Expr {

    /** The built-in "univ" signature. */
    public static final PrimSig UNIV = new PrimSig("univ", null, false);

    /** The built-in "Int" signature. */
    public static final PrimSig SIGINT = new PrimSig("Int", UNIV, false);

    /** The built-in "seq/Int" signature. */
    public static final PrimSig SEQIDX = new PrimSig("seq/Int", SIGINT, true);

    /** The built-in "String" signature. */
    public static final PrimSig STRING = new PrimSig("fun/String", UNIV, true);

    /** The built-in "none" signature. */
    public static final PrimSig NONE = new PrimSig("none", null, false);

    /** Returns the name for this sig; this name need not be unique. */
    @Override public final String toString()  { 
    	StringBuilder sb=new StringBuilder(); 
    	toString(sb, 0, false); 
    	return sb.toString(); 
    }

    /** {@inheritDoc} */
    @Override public final void toString(StringBuilder out, int indent, boolean newline) {

    	for(int i=0; i<indent && newline; i++) { 
    		out.append(' '); 
    	}
        
        
    	if (isPrivate != null)
    		out.append("private ");
    	if (isAbstract != null)
    		out.append("abstract ");
    	if (isLone != null)
    		out.append("lone ");
    	if (isOne != null)
    		out.append("one ");
    	if (isSome != null)
    		out.append("some ");
    	
   
    	out.append("sig " + label + " ");
    
    	if (isSubsig != null)
    		out.append("extends ");
    	if (isSubset != null)
    		out.append("in ");
    	
    	if (parents != null) {
    		String parentList = "";
    		for(Expr e: parents) {
    			if (parentList.length() != 0) parentList += ", ";
    			parentList += e.toString();
    		}
    		out.append(parentList);
    	}
   
    	out.append(" {");
        if (fields != null && fields.size() != 0) {
        	out.append("\n");
        	for(Decl d: fields)
        		out.append("   " + d.toString() + ",\n");
        }        
        out.append("}");
    

        if (fact != null) {       	
        	out.append(" {\n");
        	fact.toString(out, indent + 2, true);
        	out.append("\n}");
        }
    }

    /** {@inheritDoc} */
    @Override public final Pos span() { return pos; }

    
    /** {@inheritDoc} */
    @Override final<T> T accept(VisitReturn<T> visitor) throws Err { return visitor.visit(this); }

    /**
     * Nonnull if this sig is abstract.
     * <p> Note: if a sig is abstract, then it cannot and will not be a subset sig.
     */
    public final Pos isAbstract;

    /**
     * Nonnull if this sig is a PrimSig but not a builtin sig and its parent is not UNIV
     */
    public final Pos isSubsig;

    /**
     * Nonnull if this sig is a SubsetSig.
     * <p> Note: if a sig is a subset sig, then it cannot and will not be abstract.
     */
    public final Pos isSubset;

    /**
     * Nonnull if this sig's multiplicity is declared to be lone.
     * <p> Note: at most one of "lone", "one", "some" can be nonnull for each sig.
     */
    public final Pos isLone;

    /**
     * Nonnull if this sig's multiplicity is declared to be one.
     * <p> Note: at most one of "lone", "one", "some" can be nonnull for each sig.
     */
    public final Pos isOne;

    /**
     * Nonnull if this sig's multiplicity is declared to be some.
     * <p> Note: at most one of "lone", "one", "some" can be nonnull for each sig.
     */
    public final Pos isSome;

    /**
     * Nonnull if the user wanted this sig to be private.
     * <p> Note: this value is always null for builtin sigs.
     */
    public final Pos isPrivate;

    /** The label for this sig; this name does not need to be unique. */
    public final String label;

    /** */
    private final ConstList<ExprVar> parents;
    
    /** field declarations */
    private Vector<Decl> fields;
    
    /** appended fact */
    private final Expr fact;
    
 
    /** Constructs a new builtin PrimSig. */
    private Sig(String label) {
        super(Pos.UNKNOWN, null);
        this.isAbstract = null;
        this.isLone = null;
        this.isOne = null;
        this.isSome = null;
        this.label = label;
        this.isSubset = null;
        this.isSubsig = null;
        this.isPrivate = null;
        this.parents = null;
        this.fields = null;
        this.fact = null;
    }

    /** Constructs a new PrimSig or SubsetSig. */
    public Sig(Pos pos, Type type, String label, Pos abs, Pos lone, Pos one, Pos some, Pos subsig, Pos subset, Pos isPrivate, 
    		List<ExprVar> parents, List<Decl> fields, Expr facts) throws Err {
        super(pos, type);
        
        this.isPrivate = isPrivate;
        this.isAbstract = abs;
        this.isLone = lone;
        this.isOne = one;
        this.isSome = some;
        this.label = label;
        this.isSubset = subset;
        this.isSubsig = subsig;
        this.parents = ConstList.make(parents);
        this.fields = new Vector<Decl> ();
        this.fields.addAll(ConstList.make(fields));
        this.fact = facts;
    }

    
    public Sig(Pos pos, String label) throws Err { 
    	this(pos, null, label, null, null, null, null, null, null, null, null, null, null); }
    
    public Sig addFileds (List<Decl> newFields){
    	fields.addAll(newFields);
    	return this;
    }

    /** {@inheritDoc} */
    public int getDepth() { return 1; }
    
    /** Returns true iff "this is equal or subtype of that" */
    public  boolean isSameOrDescendentOf(Sig that) { return false; }

    //==============================================================================================================//


    /**
     * Mutable; reresents a non-subset signature.
     *
     * <p> Note: except for "children()", the return value of every method is always valid for all time;
     * for example, given sigs A and B, and you call C=A.intersect(B), then the result C will always be
     * the intersection of A and B even if the caller later constructs more sigs or subsigs or subsetsigs...
     */

    public static final class PrimSig extends Sig {

        /**
         * Stores its immediate children sigs (not including NONE)
         * <p> Note: if this==UNIV, then this list will always be empty, since we don't keep track of UNIV's children
         */
        private final SafeList<PrimSig> children = new SafeList<PrimSig>();

        /**
         * Returns its immediate children sigs (not including NONE)
         * <p> Note: if this==UNIV, then this method will throw an exception, since we don't keep track of UNIV's children
         */
        public SafeList<PrimSig> children() throws Err {
            if (this==UNIV) throw new ErrorFatal("Internal error (cannot enumerate the subsigs of UNIV)");
            return children.dup();
        }

        /**
         * Returns its subsigs and their subsigs and their subsigs, etc.
         * <p> Note: if this==UNIV, then this method will throw an exception, since we don't keep track of UNIV's children
         */
        public Iterable<PrimSig> descendents() throws Err {
            if (this==UNIV) throw new ErrorFatal("Internal error (cannot enumerate the subsigs of UNIV)");
            Iterable<PrimSig> answer = children.dup();
            for(PrimSig x:children) answer = Util.fastJoin(answer, x.descendents());
            return answer;
        }

        /** True if all subsigs will get this sig's type. */
        final boolean hint_isLeaf;

        /** If this is UNIV or NONE, then this field is null, else this field is the parent sig. */
        public final PrimSig parent;

        /** Constructs a builtin PrimSig. */
        private PrimSig(String label, PrimSig parent, boolean add) {
            super(label);
            this.hint_isLeaf=false;
            this.parent=parent;
            if (add) this.parent.children.add(this);
        }

        /**
         * Constructs a non-builtin sig.
         *
         * @param pos - the position in the original file where this sig was defined (can be null if unknown)
         * @param parent - the parent (must not be null, and must not be NONE)
         * @param label - the name of this sig (it does not need to be unique)
         * @param isAbstract - nonnull iff this sig should be abstract
         * @param lone - nonnull iff this sig has the "lone" multiplicity
         * @param one - nonnull iff this sig has the "one" multiplicity
         * @param some - nonnull iff this sig has the "some" multiplicity
         * @param isLeaf - true if all its future subsigs shall have the same "type" as this sig
         *
         * @throws ErrorSyntax if the signature has two or more multiplicities
         * @throws ErrorType if you attempt to extend the builtin sigs NONE, SIGINT, SEQIDX, or STRING
         */
        public PrimSig
        (Pos pos, PrimSig parent, String label, Pos isAbstract, Pos lone, Pos one, Pos some, Pos subsig, Pos isPrivate, boolean isLeaf)
        throws Err {
            super(pos,
                (parent!=null && parent.hint_isLeaf) ? parent.type : null,
                label, isAbstract, lone, one, some,
                (parent!=null && parent!=UNIV) ? Pos.UNKNOWN.merge(subsig) : null,
                null, isPrivate, null, null, null);
            if (parent==SIGINT) throw new ErrorSyntax(pos, "sig "+label+" cannot extend the builtin \"Int\" signature");
            if (parent==SEQIDX) throw new ErrorSyntax(pos, "sig "+label+" cannot extend the builtin \"seq/Int\" signature");
            if (parent==STRING) throw new ErrorSyntax(pos, "sig "+label+" cannot extend the builtin \"fun/String\" signature");
            if (parent==NONE)   throw new ErrorSyntax(pos, "sig "+label+" cannot extend the builtin \"none\" signature");
            if (parent==null) parent=UNIV; else if (parent!=UNIV) parent.children.add(this);
            this.parent = parent;
            this.hint_isLeaf = isLeaf || (parent.hint_isLeaf);
        }

        /**
         * Constructs a non-builtin sig.
         *
         * @param pos - the position in the original file where this sig was defined (can be null if unknown)
         * @param parent - the parent (must not be null, and must not be NONE)
         * @param label - the name of this sig (it does not need to be unique)
         * @param isAbstract - true iff this sig should be abstract
         * @param lone - true iff this sig has the "lone" multiplicity
         * @param one - true iff this sig has the "one" multiplicity
         * @param some - true iff this sig has the "some" multiplicity
         * @param isLeaf - true if all its future subsigs shall have the same "type" as this sig
         *
         * @throws ErrorSyntax if the signature has two or more multiplicities
         * @throws ErrorType if you attempt to extend the builtin sigs NONE, SIGINT, SEQIDX, or STRING
         */
        public PrimSig(Pos pos, PrimSig parent, String label, boolean isAbstract, boolean lone, boolean one, boolean some,
        boolean isLeaf) throws Err {
            this(pos, parent, label, isAbstract?Pos.UNKNOWN:null,
               lone?Pos.UNKNOWN:null, one?Pos.UNKNOWN:null, some?Pos.UNKNOWN:null, null, null, isLeaf);
        }

        /**
         * Constructs a non-builtin sig.
         * @param pos - the position in the original file where this sig was defined (can be null if unknown)
         * @param label - the name of this sig (it does not need to be unique)
         */
        public PrimSig(Pos pos, String label) throws Err { 
        	this(pos, null, label, null,null,null,null,null,null, false); 
        }

        /** {@inheritDoc} */
        @Override public boolean isSameOrDescendentOf(Sig that) {
            if (this==NONE || this==that || that==UNIV) return true;
            if (this==UNIV || that==NONE) return false;
            for(PrimSig me=this; me!=null; me=me.parent) if (me==that) return true;
            return false;
        }

        /** Returns the intersection between this and that (and returns "none" if they do not intersect). */
        public PrimSig intersect(PrimSig that) {
            if (this.isSameOrDescendentOf(that)) return this;
            if (that.isSameOrDescendentOf(this)) return that;
            return NONE;
        }

        /** Returns true iff the intersection between this and that is not "none". */
        public boolean intersects(PrimSig that) {
            if (this.isSameOrDescendentOf(that)) return this!=NONE;
            if (that.isSameOrDescendentOf(this)) return that!=NONE;
            return false;
        }

        /**
         * Returns the most-specific-sig that contains this and that.
         * In particular, if this extends that, then return that.
         */
        public PrimSig leastParent(PrimSig that) {
            if (isSameOrDescendentOf(that)) return that;
            PrimSig me=this;
            while(true) {
                if (that.isSameOrDescendentOf(me)) return me;
                me=me.parent;
                if (me==null) return UNIV;
            }
        }

    }

    //==============================================================================================================//
    
}
